Nuprl Lemma : fun_exp_compose
11,40
postcript
pdf
T
:Type,
n
:
,
h
,
f
:(
T
T
). (
f
^
n
o
h
) = primrec(
n
;
h
;
i
,
g
.
f
o
g
)
T
T
latex
Definitions
False
,
A
,
A
B
,
i
j
,
P
Q
,
tt
,
(
i
=
j
)
,
if
b
then
t
else
f
fi
,
Y
,
t
T
,
primrec(
n
;
b
;
c
)
,
f
^
n
,
x
:
A
.
B
(
x
)
,
f
o
g
,
,
{
T
}
,
SQType(
T
)
,
ff
,
P
&
Q
,
,
P
Q
,
P
Q
Lemmas
ge
wf
,
nat
properties
,
nat
wf
,
compose
wf
,
primrec
add
,
int
seg
wf
,
le
wf
,
primrec
wf
,
fun
exp
wf
origin
T:Type, n:
, h, f:(T
T). (f^n o h) = primrec(n;h;
i,g. f o g) 
TT T:Type, n:, h, f:(TT). (f^n o h) = primrec(n;h;i,g. f o g) TT 
A
B
j 
Q
j) Tx:A. B(x)
Q Q